(*
** Tipo de datos que representa matrices de tamaño mxn.
** Una matriz mxn se representa mediante un vector con n vectores de tamaño m.
*)

Require Import Numbers.Natural.Peano.NPeano.
Require Import Arith.EqNat.
Require Import Coq.Logic.JMeq.
Require Import Omega.


Module Matrix.
Local Set Implicit Arguments.

Inductive Vect (A:Set) : nat -> Type :=
  | vnil : Vect A 0
  | vcons : forall (n: nat), A -> Vect A n -> Vect A (S n)
.

Definition Matrix (A:Set) (n m : nat) := Vect (Vect A m) n.


Fixpoint vect_get (A:Set)(i n:nat)(v:Vect A n): option A :=
  match v with
    | vnil => None
    | vcons x a xs =>
      if ltb x i then None
      else if beq_nat x i then Some a
      else vect_get i xs
 end.

Fixpoint get (A:Set)(n m:nat)(i j:nat)(matr:Matrix A n m): option A :=
  match vect_get i matr with
    | None => None
    | Some v => vect_get j v
  end.

Fixpoint vect_set (A:Set)(i n: nat)(elem:A)(v: Vect A n): option (Vect A n) :=
  match v with
  | vnil => None
  | vcons x a xs =>
    if ltb x i then None
    else if beq_nat x i then Some (vcons elem xs)
    else
      match vect_set i elem xs with
      | None => None
      | Some v => Some (vcons a v)
      end
 end.

Fixpoint set (A:Set)(n m: nat)(i j: nat)(elem: A)(matr: Matrix A n m): option (Matrix A n m) :=
  match vect_get i matr with
    | None => None
    | Some v => 
      match vect_set j elem v with
        | None => None
        | Some v' => vect_set i v' matr
      end
  end.

Fixpoint new_vect (A:Set)(n:nat)(a:A): Vect A n :=
  match n with
    | 0 => vnil A
    | S m => vcons a (new_vect m a)
  end.

Fixpoint new_matr (A:Set)(a:A)(n m:nat): Matrix A n m :=
  match n with
    | 0 => vnil (Vect A m)
    | S x => vcons (new_vect m a) (new_matr a x m)
  end.

Functional Scheme vect_get_ind := Induction for vect_get Sort Prop.

Lemma ltb_correct : forall m n, m < n -> ltb m n = true.
Proof.
  intros.
  apply ltb_lt.
  apply H.
Qed.

Lemma ltb_complete : forall m n, ltb m n = true -> m < n.
Proof.
  intros.
  apply ltb_lt.
  apply H.
Qed.

Lemma ltb_complete_conv : forall m n, ltb n m = false -> m <= n.
Proof.
  intros m n EQ. apply not_lt.
  intro LT. apply ltb_correct in LT. rewrite LT in EQ; discriminate.
Qed.

Lemma vect_get_some : forall A m i (v : Vect A m),
  m >= 1 -> 0 <= i < m -> exists n, vect_get i v = Some n.
Proof.
  intros.
  functional induction (vect_get i v).
  omega.
  apply ltb_complete in e.
  omega.
  exists a; auto.
  apply beq_nat_false in e0.
  apply IHo; omega.
Qed.

Lemma get_some : forall A m n i j (matr : Matrix A m n),
  m >= 1 -> n >= 1 -> 0 <= i < m -> 0 <= j < n -> exists a, get i j matr = Some a.
Proof.
  intros.
  unfold get.
  destruct matr.
  inversion H.
  elim vect_get_some with (v:=(vcons v matr))(i:=i); [| assumption | assumption].
  intros.
  rewrite H3.
  apply vect_get_some; assumption.
Qed.

Functional Scheme vect_set_ind := Induction for vect_set Sort Prop.

Theorem set_vect : forall A i m a (v: Vect A m),
  m >= 1 -> 0 <= i < m -> exists v', vect_set i a v = Some v'.
Proof.
  intros.
  functional induction (vect_set i a v).
  inversion H.
  destruct H0.
  apply ltb_complete in e.
  omega.
  exists (vcons elem xs); reflexivity.
  exists (vcons a v0); reflexivity.
  elim IHo.
  intros.
  rewrite H1 in e1.
  inversion e1.
  apply ltb_complete_conv in e.
  rewrite beq_nat_false_iff in e0.
  omega.
  split.
  apply H0.
  apply ltb_complete_conv in e.
  rewrite beq_nat_false_iff in e0.
  omega.
Qed.

Theorem set_matrix : forall (i j m n: nat)(A:Set)(matr: Matrix A m n) b,
  0 <= i < m -> 0 <= j < n -> exists matr', set i j b matr = Some matr'.
Proof.
  intros.
  unfold set.
  destruct matr.
  destruct H.
  inversion H1.
  elim vect_get_some with (v:=vcons v matr)(i:=i).
  intros.
  rewrite H1.
  elim set_vect with (v:=x)(i:=j)(a:=b).
  intros.
  rewrite H2.
  elim set_vect with (v:=vcons v matr)(i:=i)(a:=x0).
  intros.
  exists x1.
  assumption.
  omega.
  omega.
  omega.
  omega.
  omega.
  omega.
Qed.

Theorem set_vect_get : forall A i m a (v v': Vect A m),
  m >= 1 -> 0 <= i < m -> vect_set i a v = Some v' -> vect_get i v' = Some a .
Proof.
  intros.
  functional induction (vect_set i a v).
  discriminate H1.
  discriminate H1.
  injection H1; intros; subst; clear H1.
  unfold vect_get.
  rewrite e.
  rewrite e0.
  reflexivity.
  injection H1; intros; subst; clear H1.
  elim IHo with (v':=v0).
  unfold vect_get.
  rewrite e.
  rewrite e0.
  reflexivity.
  apply ltb_complete_conv in e.
  rewrite beq_nat_false_iff in e0.
  omega.
  apply ltb_complete_conv in e.
  rewrite beq_nat_false_iff in e0.
  omega.
  assumption.
  discriminate H1.
Qed.

Theorem vect_set_other_get : forall (A:Set) i q m (v v': Vect A m) a b,
                        0 <= i < m ->
                        0 <= q < m ->
                        q <> i ->
                        vect_get i v = Some a ->
                        vect_set q b v = Some v' ->
                        vect_get i v' = Some a.
Proof.
  intros.
  functional induction (vect_set q b v).
  discriminate H3.
  discriminate H3.
  injection H3; intros; subst; clear H3.
  rewrite beq_nat_true_iff in e0; subst; clear e.
  destruct (q <? i) eqn:?.
  apply ltb_complete in Heqb.
  omega.
  apply beq_nat_false_iff in H1.
  simpl.
  simpl in H2.
  rewrite H1.
  rewrite H1 in H2.
  assumption.
  injection H3; intros; subst; clear H3.

  apply beq_nat_false_iff in H1.
  simpl.
  simpl in H2.
  destruct (x <? i) eqn:?.
  discriminate H2.
  destruct (beq_nat x i) eqn:?.
  assumption.
  apply (IHo v0).
  rewrite beq_nat_false_iff in Heqb0.
  omega.
  rewrite beq_nat_false_iff in e0.
  omega.
  assumption.
  assumption.
  discriminate H3.
Qed.

Theorem set_matrix_get : forall (A:Set)(i j m n:nat)(matr matr': Matrix A m n) (a:A),
  m >= 1 -> 0 <= i < m -> n >= 1 -> 0 <= j < n  -> 
  set i j a matr = Some matr' -> get i j matr' = Some a .
Proof.
  intros.
  destruct matr.
  compute in H3; discriminate H3.
  unfold set in H3.
  elim vect_get_some with (v:=vcons v matr)(i:=i); intros; [|assumption|assumption].
  rewrite H4 in H3.
  elim set_vect with (v:=x)(i:=j)(a:=a); intros; [|assumption|assumption].
  rewrite H5 in H3.
  unfold get.
  apply set_vect_get in H3; [|assumption|assumption].
  rewrite H3.
  apply set_vect_get in H5; [|assumption|assumption].
  assumption.
Qed.

Theorem get_set_other_matrix_get : forall (A:Set)i j q s m n (matr matr': Matrix A m n) a b,
                        0 <= i < m -> 0 <= j < n ->
                        0 <= q < m -> 0 <= s < n ->
                  
                        ~ ((i = q) /\ (j = s)) ->
                        get i j matr = Some a ->
                        set q s b matr = Some matr' ->
                        get i j matr' = Some a.
Proof.
  intros.
  destruct matr.
  compute in H4; discriminate H4.
  unfold get.
  unfold get in H4.
  unfold set in H5.
  destruct (beq_nat i q) eqn:?.

  (* i = q *)
  apply beq_nat_true_iff in Heqb0.
  subst.
  elim vect_get_some with (v:=vcons v matr)(i:=q); intros.
  rewrite H6 in H4; rewrite H6 in H5; clear H6.
  elim set_vect with (i:=s)(a:=b)(v:=x); intros.
  rewrite H6 in H5.
  elim vect_get_some with (v:=matr')(i:=q); intros.
  rewrite H7.
  elim vect_set_other_get with (i:=j)(q:=s)(v:=x)(v':=x0)(b:=b).
  unfold vect_set in H5.
  destruct (n0 <? q) eqn:?.
  discriminate H5.
  destruct (beq_nat n0 q) eqn:?.
  apply beq_nat_true_iff in Heqb1.
  injection H5; intros; subst; clear H5.
  unfold vect_get in H7.
  destruct (q <? q) eqn:?.
  discriminate H7.
  destruct (beq_nat q q) eqn:?.
  injection H7; intros; subst; clear H7.
  reflexivity.
  elim (beq_nat_false q q); auto.
  fold vect_set in H5.
  elim set_vect with (i:=q)(a:=x0)(v:=matr); intros.
  rewrite H8 in H5.
  injection H5; intros; subst;clear H5.
  simpl in H7.
  rewrite Heqb1 in H7.
  rewrite Heqb0 in H7.
  assert (vect_get q x2 = Some x0).
  apply set_vect_get with (i:=q)(a:=x0)(v:=matr)(v':=x2).
  apply beq_nat_false_iff in Heqb1.
  apply ltb_complete_conv in Heqb0.
  omega.
  apply beq_nat_false_iff in Heqb1.
  apply ltb_complete_conv in Heqb0.
  omega.
  exact H8.
  rewrite H5 in H7.
  injection H7; intros; subst; reflexivity.
  apply beq_nat_false_iff in Heqb1.
  apply ltb_complete_conv in Heqb0.
  omega.
  apply beq_nat_false_iff in Heqb1.
  apply ltb_complete_conv in Heqb0.
  omega.
  assumption.
  assumption.
  unfold not in H3.
  omega.
  assumption.
  assumption.
  omega.
  assumption.
  omega.
  assumption.
  omega.
  assumption.

  (* i <> q *)
  elim vect_get_some with (v:=vcons v matr)(i:=i); intros.
  rewrite H6 in H4.
  elim vect_get_some with (v:=vcons v matr)(i:=q); intros.
  rewrite H7 in H5.
  elim set_vect with (i:=s)(a:=b)(v:=x0); intros.
  rewrite H8 in H5.
  elim vect_get_some with (v:=matr')(i:=i); intros.
  rewrite H9.
  simpl in H5.
  simpl in H6.
  simpl in H7.
  destruct (n0 <? q) eqn:?.
  discriminate H7.
  destruct (beq_nat n0 q) eqn:?.
  apply beq_nat_true_iff in Heqb2; subst.
  injection H5; intros; subst; clear H5 Heqb1.
  simpl in H9.
  destruct (q <? i) eqn:?.
  discriminate H9.
  destruct (beq_nat q i) eqn:?.
  apply beq_nat_true_iff in Heqb2.
  subst.
  elim (beq_nat_false i i); auto.
  rewrite H9 in H6.
  injection H6; intros; subst; clear H6.
  assumption.
  destruct (n0 <? i) eqn:?.
  discriminate H6.
  destruct (beq_nat n0 i) eqn:?.
  injection H6; intros; subst; clear H6.
  apply beq_nat_true_iff in Heqb4; subst.
  elim set_vect with (i:=q)(a:=x1)(v:=matr); intros.
  rewrite H6 in H5.
  injection H5; intros; subst; clear H5.
  simpl in H9.
  rewrite Heqb3 in H9.
  destruct (beq_nat i i) eqn:?.
  injection H9; intros; subst; clear H9.
  assumption.
  elim (beq_nat_false i i); auto.
  apply beq_nat_false_iff in Heqb2.
  apply ltb_complete_conv in Heqb1.
  omega.
  apply beq_nat_false_iff in Heqb2.
  apply ltb_complete_conv in Heqb1.
  omega.
  apply beq_nat_false_iff in Heqb0.
  apply ltb_complete_conv in Heqb1.
  elim set_vect with (i:=q)(a:=x1)(v:=matr); intros.
  rewrite H10 in H5.
  injection H5; intros; subst; clear H5.
  simpl in H9.
  rewrite Heqb3 in H9.
  rewrite Heqb4 in H9.
  assert (vect_get i x3 = Some x).
  apply vect_set_other_get with (i:=i)(q:=q)(v:=matr)(v':=x3)(a:=x)(b:=x1).
  apply ltb_complete_conv in Heqb3.
  apply beq_nat_false_iff in Heqb4.
  omega.
  apply ltb_complete_conv in Heqb3.
  apply beq_nat_false_iff in Heqb2.
  omega.
  unfold not; intros; subst.
  omega.
  assumption.
  assumption.
  rewrite H5 in H9.
  injection H9; intros; subst; clear H9.
  assumption.
  omega.
  apply ltb_complete_conv in Heqb3.
  apply beq_nat_false_iff in Heqb2.
  omega.
  omega.
  assumption.
  omega.
  omega.
  omega.
  omega.
  omega.
  assumption.
Qed.

End Matrix.
